Termination of String Rewriting Proved Automatically
Identifieur interne : 005379 ( Main/Exploration ); précédent : 005378; suivant : 005380Termination of String Rewriting Proved Automatically
Auteurs : H. Zantema [Pays-Bas]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2005-12-01.
English descriptors
Abstract
Abstract: This paper describes how a combination of polynomial interpretations, recursive path order, RFC match-bounds, the dependency pair method, and semantic labelling can be used for automatically proving termination of an extensive class of string rewriting systems (SRSs). The tool implementing this combination of techniques is called TORPA: Termination of Rewriting Proved Automatically. All termination proofs generated by TORPA are easy to read and check; but for many of the SRSs involved, finding a termination proof would be a hard job for a human. This paper contains all underlying theory, describes how the search for a termination proof is implemented, and includes many examples.
Url:
DOI: 10.1007/s10817-005-6545-0
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002547
- to stream Istex, to step Curation: 002516
- to stream Istex, to step Checkpoint: 001232
- to stream Main, to step Merge: 005525
- to stream Main, to step Curation: 005379
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Termination of String Rewriting Proved Automatically</title><author><name sortKey="Zantema, H" sort="Zantema, H" uniqKey="Zantema H" first="H." last="Zantema">H. Zantema</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:9F47B5BB3C7D241AF1216A704A5047E8B8AB2DF8</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1007/s10817-005-6545-0</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-3R844XLL-H/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002547</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002547</idno><idno type="wicri:Area/Istex/Curation">002516</idno><idno type="wicri:Area/Istex/Checkpoint">001232</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001232</idno><idno type="wicri:doubleKey">0168-7433:2006:Zantema H:termination:of:string</idno><idno type="wicri:Area/Main/Merge">005525</idno><idno type="wicri:Area/Main/Curation">005379</idno><idno type="wicri:Area/Main/Exploration">005379</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Termination of String Rewriting Proved Automatically</title><author><name sortKey="Zantema, H" sort="Zantema, H" uniqKey="Zantema H" first="H." last="Zantema">H. Zantema</name><affiliation wicri:level="1"><country xml:lang="fr">Pays-Bas</country><wicri:regionArea>Department of Computer Science, TU Eindhoven, P.O. Box 513, 5600 MB, Eindhoven</wicri:regionArea><wicri:noRegion>Eindhoven</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Pays-Bas</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">J Autom Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2005-12-01">2005-12-01</date><biblScope unit="volume">34</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="105">105</biblScope><biblScope unit="page" to="139">139</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>match-bounds</term><term>relative termination</term><term>semantic labelling</term><term>string rewriting</term><term>termination</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper describes how a combination of polynomial interpretations, recursive path order, RFC match-bounds, the dependency pair method, and semantic labelling can be used for automatically proving termination of an extensive class of string rewriting systems (SRSs). The tool implementing this combination of techniques is called TORPA: Termination of Rewriting Proved Automatically. All termination proofs generated by TORPA are easy to read and check; but for many of the SRSs involved, finding a termination proof would be a hard job for a human. This paper contains all underlying theory, describes how the search for a termination proof is implemented, and includes many examples.</div></front></TEI><affiliations><list><country><li>Pays-Bas</li></country></list><tree><country name="Pays-Bas"><noRegion><name sortKey="Zantema, H" sort="Zantema, H" uniqKey="Zantema H" first="H." last="Zantema">H. Zantema</name></noRegion><name sortKey="Zantema, H" sort="Zantema, H" uniqKey="Zantema H" first="H." last="Zantema">H. Zantema</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005379 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005379 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:9F47B5BB3C7D241AF1216A704A5047E8B8AB2DF8
|texte= Termination of String Rewriting Proved Automatically
}}
| This area was generated with Dilib version V0.6.33. |  |